f:().
(n:. 0  f(n))
 (q:. (0 < q & (n:. m:. ((n  m) & q  f(m)))))
 (B:. n:. B  0  i < n. f(i)) 

latex

Definitions

suptype(S; T), S  T, {T}, SQType(T), i  j , A c B, ff, tt, (i = j), if b then t else f fi , Y, f o g, primrec(n;b;c), i  j < k, f^n, {i..j}, False, x. t(x), t.1, A  B, , T, True, P  Q, P  Q, A, , t  T, P & Q, x:A. B(x), x(s), P  Q, x:A. B(x), P  Q, Dec(P)

Lemmas

qsum-subsequence-qle, qle transitivity qorder, qsum-const, qsum-qle, qsum wf, decidable int equal, ge wf, nat properties, fun exp add1, int seg wf, fun exp wf, pi1 wf, qmul-qdiv-cancel, qmul comm qrng, true wf, squash wf, qmul wf, int-rational, qmul preserves qle, qless irreflexivity, qle weakening eq qorder, qless transitivity 2 qorder, qdiv wf, q-archimedean, qle wf, le wf, nat wf, int inc rationals, qless wf, rationals wf